1. Field of the Invention
The invention relates to electronic design automation, and more particularly to techniques for assertion-based verification of electronic designs.
2. Description of Related Art
An electronic design automation (EDA) system is a form of computer aided design (CAD) system used for designing integrated circuit (IC) devices. The EDA system typically receives one or more high level behavioral descriptions of an IC device (e.g., in hardware description languages like VHDL, Verilog, etc.) and translates this high level design language description into netlists of various levels of abstraction. At a higher level of abstraction, a generic netlist is typically produced based on library primitives. The generic netlist can be translated into a lower level technology-specific netlist based on a technology-specific library. A netlist describes the IC design and is composed of nodes (elements) and edges, e.g., connections between nodes, and can be represented using a directed cyclic graph structure having nodes which are connected to each other with signal lines. The netlist is typically stored in computer readable media within the EDA system and optimized, verified and otherwise processed using many well known techniques. The netlist may then be used to generate a physical device layout in mask form which can be used to directly implement structures in silicon to realize the physical IC device.
At several points in the design process, it is useful to be able to simulate and test the design, or parts of the design, to verify that it operates logically as desired. If errors are found, then the design is modified or corrected in iterative fashion as necessary. Several methods are known for testing circuit designs. In one method, software models of the design are created and the software models are tested against designer-specified test cases. In other methods, each component in the design is modeled as a state transition system and described using logic formulas. All possible behaviors of the circuit design are then exercised to confirm that the design performs in accordance with the state transition logic formulas. The latter methods are more exhaustive than the former, but can require huge amounts of time and computing power to generate and execute.
A more recent design verification method, known as assertion-based verification, involves testing a simulation of the circuit against one or more assertions describing how the circuit should behave. An “assertion” is a statement that a certain property must be true, for example, that a read_request must always be followed by a read_grant within two clock cycles. Assertions allow for automated checking that the specified property is true, and can generate automatic error messages if the property is not true. Industry organizations have defined standardized assertion languages that designers can use to specify their assertions, and for which tool vendors have developed automated checking tools.
Assertion languages often support two kinds of assertions: concurrent and immediate. Immediate assertions, sometimes also called combinational assertions, follow simulation event semantics for their execution and are executed like a statement in a procedural block. Concurrent assertions, on the other hand, are based on clock semantics and use time-sampled values of variables. Concurrent assertions are sometimes also called sequential assertions. Like many formal verification tools, concurrent assertion verification tools evaluate circuit descriptions using a cycle-based semantic, which typically relies on a clock signal or signals to drive the evaluation of the circuit. Any timing or event behavior between clock edges is abstracted away.
Tools have been developed by EDA vendors to evaluate assertions against simulations of a logic design. Typically the tool compiles the assertion language statements into one or more state machines or other automata, which are used to follow along, clock tick by clock tick, with the execution of the circuit simulation. The state machines each start running anew (begin a new “attempt”) at each clock tick, and continue until they report that their corresponding assertion expression has either passed or failed in that attempt, or the simulation terminates (in which case they report an indeterminate result). Concurrent assertions usually require many clock ticks before pass or fail can be determined, so since each new clock tick begins a new attempt, multiple instances of the state machine representing multiple attempts for a given assertion are usually executing concurrently.
In order to produce fast simulations, the state machines for assertion-based verification are usually highly optimized for speed and efficiency. Unfortunately, the resulting state machines usually bear little or no resemblance to the original assertion expression to the average user. Verification tools therefore usually report whether an assertion passed or failed, and if it failed then for which attempt it failed, but usually cannot provide any further information about the failure. Even where the tools provide information about the state of the state machine upon failure, the average user has no way to relate such information to either the assertion expression or the circuit design. Designers therefore know that the circuit design failed to perform in accordance with the assertion, but do not know whether the error was in the design or in the assertion expression, much less know where in the design or where in the assertion expression the error occurred.
The debugging process in many engineering disciplines often advantageously involves a “divide-and-conquer” methodology, in which tests are performed on successively smaller pieces until the error is isolated. But modem assertion-based verification tools do not provide any significant assistance in facilitating that process. Graphical user interface tools using the same state machine output information can help somewhat, but even these tools still have the same fundamental issue of not helping the user to divide-and-conquer the problem. In short, assertion-based verification tools to date have been able to report pass/fail, but have not been able to provide assistance in debugging either the circuit design or the assertion expression.
The problem is made worse by the trend in the EDA industry toward encouraging designers to specify more of their own assertions, as well as the trend toward much more complex assertions. In light of these problems with prior art assertion-based verification tools, there is a serious need for new mechanisms and tools that will not only report pass/fail of an assertion, but also assist the user in debugging either the circuit design or the assertion expressions themselves.